22 - Kategorien in der Programmierung [ID:10672]
50 von 568 angezeigt

Die

Dann setzen wir zum Endspurt an, letzte Vorlesung heute.

Und zwar über das Thema Monaden.

Und dann haben wir am Mittwoch noch mal eine Übung zu dem Thema.

Vielleicht zunächst mal die Motivation für Monaden, wenn man mal ganz weit zurück geht,

also bis zu ihrer Erfindung, ungefähr Ende der 60er, Anfang der 70er Jahre,

um die sich so herauskristallisiert, war, dass man mithilfe von Kategorientheorie

universelle oder allgemeine Algebra formalisieren wollte.

Also speziell den Begriff Algebraische Theorie.

Also es wird ja von manchen Leuten auch gesagt, Kategorientheorie sei eine Theorie über Theorien.

Und spätestens, wenn man mit Monaden arbeitet, dann stellt man fest,

das ist tatsächlich an der Stelle der Fall.

Und wesentlich später, so Mitte der 90er Jahre, das Paper von Mochi ist,

könnte auch Anfang der 90er Jahre gewesen sein, haben also auch die Informatiker Monaden für sich entdeckt,

nämlich da, wo es darum geht, Berechnungseffekte zu modellieren.

Wenn man über funktionale Programmiersprachen nachdenkt,

und man hat so funktionale Programme, dann passieren da häufig mal Seiteneffekte,

so was wie Exceptions, oder man möchte was schreiben oder was lesen,

oder man hat irgendwie einen Zustand, der irgendwie gespeichert wird und von der Berechnung manipuliert wird.

Und um das semantisch zu modellieren, bieten sich eben auch Monaden an.

So, der Begriff Monade selber, das ist das Wort, das gab es schon viel, viel früher,

das geht zurück auf Leibniz, das war Leibniz Beitrag zur Philosophie des Abendlandes,

und die leibnizischen Monaden, die haben überhaupt nichts mit den Monaden zu tun,

die in einer Kategorientheorie vorkommen.

Also das sind ganz andere Dinge, auch wenn man mal sich deren Definitionanführung sprechen,

also das philosophische Begriff, anschaut, dann kommt man nicht drauf, dass das irgendwas damit zu tun hat.

Ich vermute, dass die Erfinder von diesen Geräten, die wir uns jetzt gleich angucken,

einfach nach etwas gesucht haben, was es noch nicht gab in der Mathematik,

und was so ähnlich klingt wie Monoid, und da sind die auf Monaden gekommen.

Vielleicht, also es waren glaube ich auch sogar Allenberg und McGlane, vielleicht wussten die auch von den Leibniz-Monaden,

haben das bewusst überladen, aber das kann man nicht sagen.

Übrigens gibt es einige Autoren, zum Beispiel Michael Barr, die als der Begriff noch nicht so ganz sich gesetzt hat,

den Begriff Tripel benutzt haben für Monade.

Was ich unsäglich finde, weil ein Tripel ist jedes drei Tupel, ja,

aber es gibt ganze Textbücher, die nur über Tripels sprechen, also zum Beispiel dieses berühmte Barr & Wells,

Toposes, Tripels, Theories.

Ist das das Gleiche, was wir dann irgendwie in der Toposverwendung bringen?

Dieses TTT-Buch, ja, und also der Mike Barr war einer der Hauptprotagonisten,

die also diesen Begriff Tripel benutzt haben für das, was heutzutage eigentlich alle Monade nennen.

So, und was ist es nun? Also eine Monade ist tatsächlich ein Tripel,

bestehend aus, also einerseits zunächst mal einem Endofunktur auf irgendeiner Kategorie,

und Etta und Mühl, das sind zwei natürliche Transformationen.

Also das ist ein Funktur hier, so und das Etta, das ist eine natürliche Transformation vom Identitätsfunktur nach T,

das nennt man auch die Einheit der Monade, und das Mühl ist eine natürliche Transformation von T²,

also T komponiert mit sich selbst nach T, und das nennt man die Multiplikation.

Diese Begriffe, die kommen nicht von ungefähr, sondern die kommen daher, dass diese Daten jetzt

drei Axiome erfüllen müssen, die sehr stark an Monoide erinnern, also diese natürliche Transformation hier,

so dass jetzt drei Diagramme kommotieren, und zwar, dass die ersten beiden, die setzen die Einheit und die Multiplikation

in Beziehung, und wenn man sich überlegt, wie man das machen will, dann gibt es zwei Arten das zu machen,

einerseits könnte ich bei T starten und quasi die Identität, die hier komponiert ist, die ich nicht sehe,

Teil einer Videoserie :

Zugänglich über

Offener Zugang

Dauer

01:33:05 Min

Aufnahmedatum

2018-02-05

Hochgeladen am

2019-04-20 21:59:03

Sprache

de-DE

Die behandelten Themen bauen auf den Stoff von Algebra des Programmierens auf und vertieft diesen. 
Folgende weiterführende Themen werden behandelt:

  • Kategorie der CPOs; insbesondere freie CPOs, Einbettungen/Projektionen, Limes-Kolimes-Koinzidenz

  • Lokal stetige Funktoren und deren kanonische Fixpunkte; Lösung rekursiver Bereichsgleichungen insbesondere Modell des ungetyptes Lambda-Kalküls

  • freie Konstruktionen, universelle Pfeile und adjungierte Funktoren

  • Äquivalenzfunktoren

  • Monaden: Eilenberg-Moore und Kleisli-Kategorien; Freie Monaden; Becks Satz

  • evtl. Distributivgesetze, verallgemeinerte Potenzmengenkonstruktion und abstrakte GSOS-Regeln

  • evtl. Algebren und Monaden für Iteration

Lernziele und Kompetenzen:

 

Fachkompetenz Verstehen Die Studierenden erklären grundlegende Begriffe und Konzepte der Kategorientheorie und beschreiben Beispiele. Sie erklären außerdem grundlegende kategorielle Ergebnisse. Anwenden Die Studierenden wenden kategorientheoretische Konzepte und Ergebnisse an, um semantische Modelle für Programmiersprachen und Spezifikationsformalismen aufzustellen. Analysieren Die Studierenden analysieren kategorientheoretische Beweise, dieskutieren die entsprechende Argumentationen und legen diese schriftlich klar nieder. Lern- bzw. Methodenkompetenz Die Studieren lesen und verstehen Fachliteratur, die die Sprache der Kategorientheorie benutzt.
Sie sind in der Lage entsprechende mathematische Argumentationen nachzuvollziehen, zu erklären und selbst zu führen und schriftlich darzus
Einbetten
Wordpress FAU Plugin
iFrame
Teilen